\documentclass[11pt]{article}

\usepackage{k2latex.bb}                                                                                                           
\usepackage{graphicx}                                                                                                             
\usepackage{tabularx}                                                                                                             
\usepackage{multirow}                                                                                                             
\usepackage{rotating}                                                                                                             
\usepackage{tikz}                                                                                                                 
\usepackage{amsmath}                                                                                                              
\usepackage{amssymb}                                                                                                              
\usepackage{amsthm}                                                                                                               
\usepackage{import}                                                                                                               
\usepackage{mathabx}                                                                                                              
\usepackage{alltt}                                                                                                                
\usepackage[noline,boxruled]{algorithm2e}   

\hoffset=-1cm
\textwidth=14cm
\marginparwidth=25pt
\topmargin=-2cm
%\footskip=4cm
\textheight=22cm

\begin{document}

% title
\title{On Compiling K Definitions}%
\author{Andrei Arusoaie\\Faculty of Computer Science, Alexandru Ioan Cuza University, Romania\\\texttt{\{andrei.arusoaie\}$@$info.uaic.ro}}%
%\today
\date{}
\maketitle%




A large part of today's programming languages research and development effort is motivated by the new requirements arising from hardware evolution and software development. Programming languages are becoming more and more complex and this is the reason why we need precise specifications and tools for defining, testing and analyzing them. One of the most effective ways to define a programming language or paradigm is as an executable formal specification which can both execute programs and formally reason about them. A framework aiming at this goal is \K. \K is a rewriting-based \cite{rewriting} semantic definitional framework which started in 2003 as a means to define executable concurrent languages in Maude. A detailed description of \K can be found in \cite{jlap2010}, and the first prototype of \K, called K-Maude, is described in \cite{wrla2010}.

Programming languages, calculi, type systems, or formal analysis tools can be defined in \K using {\it configurations}, {\it computations}, and {\it rules}. {\it Configurations} organize the system/program state in units called cells, which are labeled and can be nested. {\it Computations} carry computational meaning as special nested list structures sequentializing computational tasks, such as fragments of program; in particular, computations extend the original language or calculus syntax. \K (rewrite) {\it rules} generalize conventional rewrite rules by making explicit which parts of the term they read, write, or do not care about \cite{jlap2010}. \K scales well in giving semantics to programming languages. Until now, besides smaller and paradigmatic languages used for teaching, several important languages were defined: C \cite{csem}, Java 1.4 \cite{java}, Scheme \cite{scheme1, scheme2} and Verilog \cite{verilog}. \K is now used in teaching programming languages courses in universities from United States, Romania, and Spain.

This paper aims to solve one of the most complex transformation steps from the compilation process of a \K definition. This step is called {\it contextual transformation} and its main purpose is to increase modularity and level of abstraction of the definition. The role of contextual transformations is to transform a \K rule into a rewrite rule according to a given configuration. 

When giving semantics to a programming language in \K, one specifies the syntax using BNF (Backus-Naur Form) and the semantics using configurations and rules. The program configuration is a structure which contains the context needed for computation. Configurations are nested structures of cells which can contain standard items as environments, stores or other items specific to the given semantics. The rewrite mechanism of \K is to apply \K rules over a configuration (which modify the configuration) until no rules can be applied. In rules, one can specify only the cells of interest, or, in other words, the cells with relevant content for the current rewrite. 



\begin{figure}[h]
\centering
\begin{minipage}{\textwidth}
\fontsize{9}{9}\selectfont
\kconfig[\hspace{-12em}]{\kallLarge{red}{T}{\kallLarge{orange}{threads}{\kallLarge{yellow}{thread *}{\kallLarge{green}{k}{\variable{K}{K}}\mathrel{}\kallLarge{violet}{env}{\dotCt{Map}}\mathrel{}\kallLarge{black}{holds}{\dotCt{Map}}\kBR\kallLarge{cyan}{control}{\kallLarge{blue}{fstack}{\dotCt{List}}\mathrel{}\kallLarge{purple}{xstack}{\dotCt{List}}}}}\mathrel{}\kBR \mathrel{}\kallLarge{pink}{genv}{\dotCt{Map}}\mathrel{}\kallLarge{white}{store}{\dotCt{Map}}\mathrel{}\kallLarge{cyan}{busy}{\dotCt{Set}}\kBR\mathrel{}\kallLarge{magenta}{in}{\dotCt{List}}\mathrel{}\kallLarge{brown}{out}{\dotCt{List}}\mathrel{}\kallLarge{gray}{nextLoc}{\constant{0}{Zero}}}}
\end{minipage}\\
\caption{SIMPLE: configuration}
\label{config:S}
\end{figure}




For example, a rule which corresponds to variable lookup (Figure \ref{look}) in K definition of SIMPLE \cite{kpage} language specifies only the cell which contains the computation (the variable lookup in memory) and the cell which contains the memory. The rest of the configuration (Figure \ref{config:S}) remains the same. The problem now, is that the left hand side of this rule could not match the configuration in this form because some cells are missing and the matching algorithm is not able to infer the cell structure. This is the place where contextual transformations are needed: they infer the missing cells from configuration taking care of different cell properties. 

\begin{figure}[h]
%\centering
\begin{minipage}{.8\textwidth}
\krule[(a)\ \ ]{}{\ensuremath{{{{\kprefix{green}{k}{\reduce{\variable{X}{Id}}{\variable{V}{Val}}}}\mathrel{\terminal{}}{\kmiddle{violet}{env}{{{\variable{X}{Id}}\mathrel{\terminal{\ensuremath{\mapsto}}}{\variable{L}{Nat}}}}}}}\mathrel{\terminal{}}{\kmiddle{white}{store}{{{\variable{L}{Nat}}\mathrel{\terminal{\ensuremath{\mapsto}}}{\variable{V}{Val}}}}}}}
%(A) 
%\end{minipage}\\

%\medskip
%{\centering
\hspace{5cm}{\Huge $\downarrow$}
%}
%\medskip

%\centering
%\begin{minipage}{.9\textwidth}
%(B)
\krule[(b)\ \ ]{}{\ensuremath \kmiddle{red}{T}{{{\kmiddle{orange}{threads}{\kmiddle{yellow}{thread}{{{\kprefix{green}{k}{\reduce{\variable{X}{Id}}{\variable{V}{Val}}}}\mathrel{\terminal{}}{\kmiddle{violet}{env}{{{\variable{X}{Id}}\mathrel{\terminal{\ensuremath{\mapsto}}}{\variable{L}{Nat}}}}}}}}}\mathrel{\terminal{}}{\kmiddle{white}{store}{{{\variable{L}{Nat}}\mathrel{\terminal{\ensuremath{\mapsto}}}{\variable{V}{Val}}}}}}}}
\end{minipage}\\

\caption{SIMPLE: variable lookup rule before (a) and after (b) contextual transformation}
\label{look}
\end{figure}


Because of contextual transformations, \K has two big advantages: 
\begin{itemize}
\item abstraction, given by the fact that a user specifies in an abstract way the items of interest from configuration without caring about the concrete configuration, and 
\item modularity, given by the fact that in an existing definition a user can add more items in the configuration and rules without modifying the initial definition
\end{itemize}


The current implementation of context transformers has some limitations and its formal definitions are not completely figured out. Complex definitions, like the C semantics for instance, show that sometimes the existing algorithm leads to unexpected behaviors.\\\\




\section{Contextual transformations}
\label{ct:ex}
This section contains some examples of \K rules and their corresponding contexts  (or rewrite rules) in order to explain better the transformation process and the aspects we have to consider when giving formal definitions.\\

Recall the variable look-up rule shown in figure \ref{look} (a). In that rule, we specify only cells {\it k}, {\it env}, and {\it store}. We have to notice, that this cells are not at the same level in configuration: cells {\it k} and {\it env} are inside cell {\it thread} which is inside {\it threads} and cell {\it store} is at the same level with cell {\it threads}, both being included in top cell {\it T}. Because \K is based on rewriting this rule has to be transformed into a rewriting rule, in the sense that its left hand side has to match a term (in our case the configuration - Figure \ref{config:S}) in order to rewrite it with the right hand side. For this reason, our rule has to be filled with cells from configuration in order to be matched and applied. This is what contextual transformation should do: to transform a \K rule into a rewriting rule. It has to detect the levels of cells and to put them together until a term which can match the configuration is reached. The full context of variable lookup rule is shown in Figure \ref{look:full}


\begin{figure}[h]
\centering
\begin{minipage}{.9\textwidth}
 \krule{}{\ensuremath \kmiddle{red}{T}{{{\kmiddle{orange}{threads}{\kmiddle{yellow}{thread}{{{\kprefix{green}{k}{\reduce{\variable{X}{Id}}{\variable{V}{Val}}}}\mathrel{\terminal{}}{\kmiddle{violet}{env}{{{\variable{X}{Id}}\mathrel{\terminal{\ensuremath{\mapsto}}}{\variable{L}{Nat}}}}}}}}}\mathrel{\terminal{}}{\kmiddle{white}{store}{{{\variable{L}{Nat}}\mathrel{\terminal{\ensuremath{\mapsto}}}{\variable{V}{Val}}}}}}}}
\end{minipage}\\
\caption{SIMPLE: full context for variable lookup rule}
\label{look:full}
\end{figure}




In the next examples we will use the ASCII notation for \K rules.
The thread creation rule from SIMPLE semantics is given as the basic example of what is contextual transformations.

\begin{figure}[h]
\centering
\begin{tabular}{| c |}
\hline
\begin{minipage}{.8\textwidth}
\footnotesize
\begin{alltt}
rule     <thread_> 
                \textcolor{red}{<k> spawn S => . <_/k> <env> Env </env> }
         <_/thread>
   (. => <thread_> 
               \textcolor{red}{<k> S </k> <env> Env </env>} 
         <_/thread>)
\end{alltt}
\end{minipage}\\
\hline
\end{tabular}
\caption{Thread creation rule - SIMPLE semantics}
\label{thread:one}
\end{figure}

As we can observe in Figure \ref{thread:one}, it contains only the cells {\it thread}, {\it k} and {\it env}. When in a {\it thread} cell the \verb=spawn S= statement has to be executed then a new thread is created having the instruction set \verb=S= and the same environment \verb=Env= as its creator thread. 
\begin{figure}[h]
\centering
\begin{tabular}{| c |}
\hline
\begin{minipage}{.8\textwidth}
\footnotesize
\begin{alltt}
rule <T>
        <threads>
          <thread_> 
                \textcolor{red}{ <k> spawn S => . <_/k> <env> Env </env> } 
           <_/thread>                                
        (. => <thread_> 
                 \textcolor{red}{<k> S </k> <env> Env </env>}                                                                               
            <_/thread>)
        </threads>
     </T> 
\end{alltt}
\end{minipage}\\
\hline
\end{tabular}
\caption{Thread creation rule full context - SIMPLE semantics}
\label{none}
\end{figure}\\
The given rule is a \K rule in the sense the it is not yet a rewrite rule which is ready to be executed by a rewrite engine. The contextual transformation should add here the missing cells from configuration until the rule matches the configuration and the rewrite can succeed. So, in order to get the context of the rule shown in Figure \ref{thread:one} {\it context transformers} algorithm should receive as input that rule and should output the rule shown in Figure \ref{none}. As we can observe two other cells were added. Actually there were added as many cells as needed in order to fit the configuration. 


\section{Conclusions and future work}
There are also other problems which have to be solved when doing context transformers. Cell creation/deletion are special cases of transformations: when splitting rule in rhs and lhs we have to keep additional information about the {\it rewrite points} (nodes which are created/deleted). Consider the following rule:
\begin{verbatim}
               rule . => <cell> .Bag </cell>
\end{verbatim}
How can we apply context transformers on this rule? We can observe that splitting the rule into lhs and rhs causes more problems because the lhs is "\verb=.=" and we do not have any information about it. Supposing we have somehow the contexts for both lhs and rhs how can we combine them? What are the nodes which have to be rewritten? The answer of these questions stays in storing more information about cell involved in rewrite operations before splitting the rule. Also, looking on the other side could help when finding the context of "\verb=.=". In our case, the context of "\verb=.=" is given by the first (bottom-up) parent of cell {\it cell} which has multiplicity {\it ANY} or {\it SOME}. \\

Another issue is related to lhs and rhs. Because they are separate trees we can find contexts for each of them but we have to merge them back. The other transformations depend on this merging. The problem is that if at least one of them is ambiguous then we have to disambiguate. When merging, we should also take care of compatibility of contexts for lhs and rhs which is not necessarily easy.


\bibliographystyle{plain}
\bibliography{mibib}


\end{document}